YES 1.72 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((lookup :: Eq b => Maybe b  ->  [(Maybe b,a)]  ->  Maybe a) :: Eq b => Maybe b  ->  [(Maybe b,a)]  ->  Maybe a)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((lookup :: Eq a => Maybe a  ->  [(Maybe a,b)]  ->  Maybe b) :: Eq a => Maybe a  ->  [(Maybe a,b)]  ->  Maybe b)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
lookup k [] = Nothing
lookup k ((x,y: xys)
 | k == x
 = Just y
 | otherwise
 = lookup k xys

is transformed to
lookup k [] = lookup3 k []
lookup k ((x,y: xys) = lookup2 k ((x,y: xys)

lookup1 k x y xys True = Just y
lookup1 k x y xys False = lookup0 k x y xys otherwise

lookup0 k x y xys True = lookup k xys

lookup2 k ((x,y: xys) = lookup1 k x y xys (k == x)

lookup3 k [] = Nothing
lookup3 xy xz = lookup2 xy xz



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (lookup :: Eq a => Maybe a  ->  [(Maybe a,b)]  ->  Maybe b)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu2900), Succ(yu40001000)) → new_primPlusNat(yu2900, yu40001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu30100), Succ(yu4000100)) → new_primMulNat(yu30100, Succ(yu4000100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yu3000), Succ(yu400000)) → new_primEqNat(yu3000, yu400000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs1(@2(yu300, yu301), @2(yu40000, yu40001), app(app(app(ty_@3, gd), ge), gf), gc) → new_esEs0(yu300, yu40000, gd, ge, gf)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, app(app(ty_@2, ec), ed), cd) → new_esEs1(yu301, yu40001, ec, ed)
new_esEs1(@2(yu300, yu301), @2(yu40000, yu40001), app(app(ty_Either, ha), hb), gc) → new_esEs2(yu300, yu40000, ha, hb)
new_esEs3(:(yu300, yu301), :(yu40000, yu40001), app(ty_[], beb)) → new_esEs3(yu300, yu40000, beb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, cc, app(ty_[], ga)) → new_esEs3(yu302, yu40002, ga)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(ty_Either, dc), dd), cc, cd) → new_esEs2(yu300, yu40000, dc, dd)
new_esEs1(@2(yu300, yu301), @2(yu40000, yu40001), app(ty_[], hc), gc) → new_esEs3(yu300, yu40000, hc)
new_esEs(Just(yu300), Just(yu40000), app(app(app(ty_@3, bb), bc), bd)) → new_esEs0(yu300, yu40000, bb, bc, bd)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(ty_[], de), cc, cd) → new_esEs3(yu300, yu40000, de)
new_esEs2(Right(yu300), Right(yu40000), bbh, app(app(app(ty_@3, bcb), bcc), bcd)) → new_esEs0(yu300, yu40000, bcb, bcc, bcd)
new_esEs3(:(yu300, yu301), :(yu40000, yu40001), app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs0(yu300, yu40000, bdc, bdd, bde)
new_esEs(Just(yu300), Just(yu40000), app(app(ty_Either, bg), bh)) → new_esEs2(yu300, yu40000, bg, bh)
new_esEs(Just(yu300), Just(yu40000), app(ty_[], ca)) → new_esEs3(yu300, yu40000, ca)
new_esEs2(Right(yu300), Right(yu40000), bbh, app(app(ty_@2, bce), bcf)) → new_esEs1(yu300, yu40000, bce, bcf)
new_esEs2(Left(yu300), Left(yu40000), app(app(ty_Either, bbe), bbf), bag) → new_esEs2(yu300, yu40000, bbe, bbf)
new_esEs(Just(yu300), Just(yu40000), app(ty_Maybe, ba)) → new_esEs(yu300, yu40000, ba)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, app(app(app(ty_@3, dh), ea), eb), cd) → new_esEs0(yu301, yu40001, dh, ea, eb)
new_esEs3(:(yu300, yu301), :(yu40000, yu40001), bec) → new_esEs3(yu301, yu40001, bec)
new_esEs2(Left(yu300), Left(yu40000), app(ty_[], bbg), bag) → new_esEs3(yu300, yu40000, bbg)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, app(ty_[], eg), cd) → new_esEs3(yu301, yu40001, eg)
new_esEs2(Left(yu300), Left(yu40000), app(ty_Maybe, baf), bag) → new_esEs(yu300, yu40000, baf)
new_esEs1(@2(yu300, yu301), @2(yu40000, yu40001), hd, app(app(ty_@2, baa), bab)) → new_esEs1(yu301, yu40001, baa, bab)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, cc, app(app(ty_@2, fd), ff)) → new_esEs1(yu302, yu40002, fd, ff)
new_esEs3(:(yu300, yu301), :(yu40000, yu40001), app(app(ty_@2, bdf), bdg)) → new_esEs1(yu300, yu40000, bdf, bdg)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, cc, app(app(app(ty_@3, fa), fb), fc)) → new_esEs0(yu302, yu40002, fa, fb, fc)
new_esEs2(Right(yu300), Right(yu40000), bbh, app(ty_Maybe, bca)) → new_esEs(yu300, yu40000, bca)
new_esEs1(@2(yu300, yu301), @2(yu40000, yu40001), app(app(ty_@2, gg), gh), gc) → new_esEs1(yu300, yu40000, gg, gh)
new_esEs2(Right(yu300), Right(yu40000), bbh, app(app(ty_Either, bcg), bch)) → new_esEs2(yu300, yu40000, bcg, bch)
new_esEs1(@2(yu300, yu301), @2(yu40000, yu40001), hd, app(app(ty_Either, bac), bad)) → new_esEs2(yu301, yu40001, bac, bad)
new_esEs1(@2(yu300, yu301), @2(yu40000, yu40001), hd, app(ty_[], bae)) → new_esEs3(yu301, yu40001, bae)
new_esEs2(Right(yu300), Right(yu40000), bbh, app(ty_[], bda)) → new_esEs3(yu300, yu40000, bda)
new_esEs3(:(yu300, yu301), :(yu40000, yu40001), app(app(ty_Either, bdh), bea)) → new_esEs2(yu300, yu40000, bdh, bea)
new_esEs(Just(yu300), Just(yu40000), app(app(ty_@2, be), bf)) → new_esEs1(yu300, yu40000, be, bf)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(ty_@2, da), db), cc, cd) → new_esEs1(yu300, yu40000, da, db)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, app(ty_Maybe, dg), cd) → new_esEs(yu301, yu40001, dg)
new_esEs1(@2(yu300, yu301), @2(yu40000, yu40001), app(ty_Maybe, gb), gc) → new_esEs(yu300, yu40000, gb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, cc, app(app(ty_Either, fg), fh)) → new_esEs2(yu302, yu40002, fg, fh)
new_esEs1(@2(yu300, yu301), @2(yu40000, yu40001), hd, app(ty_Maybe, he)) → new_esEs(yu301, yu40001, he)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, app(app(ty_Either, ee), ef), cd) → new_esEs2(yu301, yu40001, ee, ef)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), df, cc, app(ty_Maybe, eh)) → new_esEs(yu302, yu40002, eh)
new_esEs3(:(yu300, yu301), :(yu40000, yu40001), app(ty_Maybe, bdb)) → new_esEs(yu300, yu40000, bdb)
new_esEs2(Left(yu300), Left(yu40000), app(app(ty_@2, bbc), bbd), bag) → new_esEs1(yu300, yu40000, bbc, bbd)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(ty_Maybe, cb), cc, cd) → new_esEs(yu300, yu40000, cb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(app(ty_@3, ce), cf), cg), cc, cd) → new_esEs0(yu300, yu40000, ce, cf, cg)
new_esEs1(@2(yu300, yu301), @2(yu40000, yu40001), hd, app(app(app(ty_@3, hf), hg), hh)) → new_esEs0(yu301, yu40001, hf, hg, hh)
new_esEs2(Left(yu300), Left(yu40000), app(app(app(ty_@3, bah), bba), bbb), bag) → new_esEs0(yu300, yu40000, bah, bba, bbb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup(Just(yu30), :(@2(Just(yu4000), yu401), yu41), ba, bb) → new_lookup1(yu30, yu4000, yu401, yu41, new_esEs4(yu30, yu4000, bb), ba, bb)
new_lookup1(yu11, yu12, yu13, yu14, False, bc, bd) → new_lookup(Just(yu11), yu14, bc, bd)
new_lookup(Nothing, :(@2(Just(yu4000), yu401), yu41), ba, bb) → new_lookup(Nothing, yu41, ba, bb)
new_lookup(Just(yu30), :(@2(Nothing, yu401), yu41), ba, bb) → new_lookup(Just(yu30), yu41, ba, bb)

The TRS R consists of the following rules:

new_esEs21(yu300, yu40000, ty_Double) → new_esEs6(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Float) → new_esEs5(yu302, yu40002)
new_primPlusNat1(Succ(yu2900), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu2900, yu40001000)))
new_esEs25(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Double) → new_esEs6(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Char) → new_esEs15(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_esEs21(yu300, yu40000, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs6(yu30, yu4000)
new_esEs9(LT, GT) → False
new_esEs9(GT, LT) → False
new_esEs16(Left(yu300), Left(yu40000), app(ty_[], fc), ce) → new_esEs18(yu300, yu40000, fc)
new_esEs24(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs18(:(yu300, yu301), :(yu40000, yu40001), cf) → new_asAs(new_esEs24(yu300, yu40000, cf), new_esEs18(yu301, yu40001, cf))
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_esEs24(yu300, yu40000, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs23(yu302, yu40002, app(ty_Ratio, bbd)) → new_esEs10(yu302, yu40002, bbd)
new_esEs22(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs21(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs26(yu301, yu40001, app(ty_Ratio, bfb)) → new_esEs10(yu301, yu40001, bfb)
new_esEs26(yu301, yu40001, ty_Double) → new_esEs6(yu301, yu40001)
new_esEs21(yu300, yu40000, ty_Bool) → new_esEs17(yu300, yu40000)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs23(yu302, yu40002, app(app(app(ty_@3, bbe), bbf), bbg)) → new_esEs11(yu302, yu40002, bbe, bbf, bbg)
new_esEs4(yu30, yu4000, app(app(app(ty_@3, bg), bh), ca)) → new_esEs11(yu30, yu4000, bg, bh, ca)
new_esEs22(yu301, yu40001, ty_Bool) → new_esEs17(yu301, yu40001)
new_esEs9(GT, GT) → True
new_esEs24(yu300, yu40000, app(app(ty_@2, bdb), bdc)) → new_esEs13(yu300, yu40000, bdb, bdc)
new_esEs25(yu300, yu40000, ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), ty_Double) → new_esEs6(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Char) → new_esEs15(yu301, yu40001)
new_esEs26(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs24(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Char) → new_esEs15(yu302, yu40002)
new_esEs23(yu302, yu40002, app(ty_Maybe, bbc)) → new_esEs8(yu302, yu40002, bbc)
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs16(Left(yu300), Left(yu40000), app(ty_Maybe, eb), ce) → new_esEs8(yu300, yu40000, eb)
new_esEs17(True, True) → True
new_esEs8(Just(yu300), Just(yu40000), app(app(ty_@2, de), df)) → new_esEs13(yu300, yu40000, de, df)
new_esEs16(Right(yu300), Right(yu40000), cd, app(app(ty_Either, gd), ge)) → new_esEs16(yu300, yu40000, gd, ge)
new_esEs8(Just(yu300), Just(yu40000), app(app(app(ty_@3, db), dc), dd)) → new_esEs11(yu300, yu40000, db, dc, dd)
new_esEs23(yu302, yu40002, ty_Double) → new_esEs6(yu302, yu40002)
new_esEs25(yu300, yu40000, app(app(app(ty_@3, bea), beb), bec)) → new_esEs11(yu300, yu40000, bea, beb, bec)
new_esEs16(Right(yu300), Right(yu40000), cd, app(ty_[], gf)) → new_esEs18(yu300, yu40000, gf)
new_esEs4(yu30, yu4000, app(app(ty_@2, cb), cc)) → new_esEs13(yu30, yu4000, cb, cc)
new_esEs23(yu302, yu40002, ty_Integer) → new_esEs12(yu302, yu40002)
new_esEs16(Right(yu300), Right(yu40000), cd, app(ty_Maybe, fd)) → new_esEs8(yu300, yu40000, fd)
new_esEs12(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs22(yu301, yu40001, ty_Float) → new_esEs5(yu301, yu40001)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Ordering) → new_esEs9(yu302, yu40002)
new_esEs16(Left(yu300), Left(yu40000), app(app(app(ty_@3, ed), ee), ef), ce) → new_esEs11(yu300, yu40000, ed, ee, ef)
new_esEs26(yu301, yu40001, app(app(ty_@2, bff), bfg)) → new_esEs13(yu301, yu40001, bff, bfg)
new_esEs21(yu300, yu40000, app(ty_Ratio, gh)) → new_esEs10(yu300, yu40000, gh)
new_esEs8(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs9(yu300, yu40000)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs11(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), bg, bh, ca) → new_asAs(new_esEs21(yu300, yu40000, bg), new_asAs(new_esEs22(yu301, yu40001, bh), new_esEs23(yu302, yu40002, ca)))
new_esEs25(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs18([], :(yu40000, yu40001), cf) → False
new_esEs18(:(yu300, yu301), [], cf) → False
new_esEs23(yu302, yu40002, app(app(ty_@2, bbh), bca)) → new_esEs13(yu302, yu40002, bbh, bca)
new_esEs16(Left(yu300), Left(yu40000), app(app(ty_Either, fa), fb), ce) → new_esEs16(yu300, yu40000, fa, fb)
new_esEs16(Left(yu300), Left(yu40000), ty_Bool, ce) → new_esEs17(yu300, yu40000)
new_esEs22(yu301, yu40001, ty_Integer) → new_esEs12(yu301, yu40001)
new_esEs16(Left(yu300), Right(yu40000), cd, ce) → False
new_esEs16(Right(yu300), Left(yu40000), cd, ce) → False
new_esEs26(yu301, yu40001, app(app(app(ty_@3, bfc), bfd), bfe)) → new_esEs11(yu301, yu40001, bfc, bfd, bfe)
new_esEs23(yu302, yu40002, ty_Bool) → new_esEs17(yu302, yu40002)
new_esEs9(EQ, GT) → False
new_esEs9(GT, EQ) → False
new_esEs5(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs14(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs25(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), app(app(ty_Either, dg), dh)) → new_esEs16(yu300, yu40000, dg, dh)
new_esEs8(Nothing, Nothing, be) → True
new_esEs4(yu30, yu4000, app(ty_Maybe, be)) → new_esEs8(yu30, yu4000, be)
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs4(yu30, yu4000, app(ty_Ratio, bf)) → new_esEs10(yu30, yu4000, bf)
new_esEs21(yu300, yu40000, app(app(ty_@2, hd), he)) → new_esEs13(yu300, yu40000, hd, he)
new_esEs8(Just(yu300), Just(yu40000), ty_Int) → new_esEs14(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Double, ce) → new_esEs6(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Int) → new_esEs14(yu301, yu40001)
new_esEs19(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Ordering, ce) → new_esEs9(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Int) → new_esEs14(yu302, yu40002)
new_asAs(False, yu28) → False
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs8(Just(yu300), Just(yu40000), ty_@0) → new_esEs7(yu300, yu40000)
new_primEqNat0(Zero, Zero) → True
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs22(yu301, yu40001, app(ty_Maybe, baa)) → new_esEs8(yu301, yu40001, baa)
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_esEs18([], [], cf) → True
new_esEs25(yu300, yu40000, app(ty_[], beh)) → new_esEs18(yu300, yu40000, beh)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_[], bdf)) → new_esEs18(yu300, yu40000, bdf)
new_esEs22(yu301, yu40001, app(app(ty_Either, bah), bba)) → new_esEs16(yu301, yu40001, bah, bba)
new_esEs17(False, False) → True
new_esEs8(Just(yu300), Just(yu40000), ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, app(ty_[], cf)) → new_esEs18(yu30, yu4000, cf)
new_esEs17(False, True) → False
new_esEs17(True, False) → False
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs12(yu30, yu4000)
new_esEs21(yu300, yu40000, app(app(ty_Either, hf), hg)) → new_esEs16(yu300, yu40000, hf, hg)
new_esEs21(yu300, yu40000, app(ty_Maybe, gg)) → new_esEs8(yu300, yu40000, gg)
new_esEs15(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Integer, ce) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs26(yu301, yu40001, app(app(ty_Either, bfh), bga)) → new_esEs16(yu301, yu40001, bfh, bga)
new_esEs23(yu302, yu40002, ty_@0) → new_esEs7(yu302, yu40002)
new_esEs21(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), app(app(ty_@2, eg), eh), ce) → new_esEs13(yu300, yu40000, eg, eh)
new_esEs13(@2(yu300, yu301), @2(yu40000, yu40001), cb, cc) → new_asAs(new_esEs25(yu300, yu40000, cb), new_esEs26(yu301, yu40001, cc))
new_esEs16(Right(yu300), Right(yu40000), cd, app(app(ty_@2, gb), gc)) → new_esEs13(yu300, yu40000, gb, gc)
new_esEs8(Just(yu300), Just(yu40000), ty_Char) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Ratio, bcf)) → new_esEs10(yu300, yu40000, bcf)
new_esEs23(yu302, yu40002, app(app(ty_Either, bcb), bcc)) → new_esEs16(yu302, yu40002, bcb, bcc)
new_esEs22(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_primPlusNat0(Succ(yu290), yu4000100) → Succ(Succ(new_primPlusNat1(yu290, yu4000100)))
new_esEs20(yu301, yu40001, ty_Integer) → new_esEs12(yu301, yu40001)
new_esEs16(Left(yu300), Left(yu40000), ty_Int, ce) → new_esEs14(yu300, yu40000)
new_esEs22(yu301, yu40001, app(ty_[], bbb)) → new_esEs18(yu301, yu40001, bbb)
new_esEs22(yu301, yu40001, app(ty_Ratio, bab)) → new_esEs10(yu301, yu40001, bab)
new_esEs21(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), app(ty_Ratio, da)) → new_esEs10(yu300, yu40000, da)
new_esEs26(yu301, yu40001, ty_Integer) → new_esEs12(yu301, yu40001)
new_esEs8(Nothing, Just(yu40000), be) → False
new_esEs8(Just(yu300), Nothing, be) → False
new_esEs9(EQ, EQ) → True
new_esEs14(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu300, yu40000, ty_Double) → new_esEs6(yu300, yu40000)
new_esEs22(yu301, yu40001, app(app(ty_@2, baf), bag)) → new_esEs13(yu301, yu40001, baf, bag)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs26(yu301, yu40001, app(ty_Maybe, bfa)) → new_esEs8(yu301, yu40001, bfa)
new_primPlusNat1(Succ(yu2900), Zero) → Succ(yu2900)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs25(yu300, yu40000, ty_Char) → new_esEs15(yu300, yu40000)
new_esEs25(yu300, yu40000, app(ty_Ratio, bdh)) → new_esEs10(yu300, yu40000, bdh)
new_esEs21(yu300, yu40000, ty_Char) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Maybe, bce)) → new_esEs8(yu300, yu40000, bce)
new_esEs26(yu301, yu40001, ty_Bool) → new_esEs17(yu301, yu40001)
new_esEs9(LT, EQ) → False
new_esEs9(EQ, LT) → False
new_esEs20(yu301, yu40001, ty_Int) → new_esEs14(yu301, yu40001)
new_esEs21(yu300, yu40000, app(ty_[], hh)) → new_esEs18(yu300, yu40000, hh)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs4(yu30, yu4000, app(app(ty_Either, cd), ce)) → new_esEs16(yu30, yu4000, cd, ce)
new_esEs25(yu300, yu40000, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs15(yu30, yu4000)
new_esEs19(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_esEs25(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), app(ty_Ratio, ec), ce) → new_esEs10(yu300, yu40000, ec)
new_esEs22(yu301, yu40001, ty_Int) → new_esEs14(yu301, yu40001)
new_esEs24(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs26(yu301, yu40001, app(ty_[], bgb)) → new_esEs18(yu301, yu40001, bgb)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs26(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs25(yu300, yu40000, ty_Double) → new_esEs6(yu300, yu40000)
new_asAs(True, yu28) → yu28
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs22(yu301, yu40001, ty_Double) → new_esEs6(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_@0) → new_esEs7(yu30, yu4000)
new_esEs24(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), app(ty_Maybe, cg)) → new_esEs8(yu300, yu40000, cg)
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_esEs22(yu301, yu40001, app(app(app(ty_@3, bac), bad), bae)) → new_esEs11(yu301, yu40001, bac, bad, bae)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs14(yu30, yu4000)
new_esEs16(Right(yu300), Right(yu40000), cd, app(ty_Ratio, ff)) → new_esEs10(yu300, yu40000, ff)
new_esEs24(yu300, yu40000, app(app(app(ty_@3, bcg), bch), bda)) → new_esEs11(yu300, yu40000, bcg, bch, bda)
new_esEs26(yu301, yu40001, ty_Float) → new_esEs5(yu301, yu40001)
new_esEs8(Just(yu300), Just(yu40000), ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Char, ce) → new_esEs15(yu300, yu40000)
new_esEs21(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, app(app(ty_Either, bdd), bde)) → new_esEs16(yu300, yu40000, bdd, bde)
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs8(Just(yu300), Just(yu40000), app(ty_[], ea)) → new_esEs18(yu300, yu40000, ea)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Char) → new_esEs15(yu300, yu40000)
new_esEs6(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs14(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs25(yu300, yu40000, app(app(ty_@2, bed), bee)) → new_esEs13(yu300, yu40000, bed, bee)
new_esEs10(:%(yu300, yu301), :%(yu40000, yu40001), bf) → new_asAs(new_esEs19(yu300, yu40000, bf), new_esEs20(yu301, yu40001, bf))
new_esEs25(yu300, yu40000, app(app(ty_Either, bef), beg)) → new_esEs16(yu300, yu40000, bef, beg)
new_esEs7(@0, @0) → True
new_esEs23(yu302, yu40002, app(ty_[], bcd)) → new_esEs18(yu302, yu40002, bcd)
new_esEs21(yu300, yu40000, app(app(app(ty_@3, ha), hb), hc)) → new_esEs11(yu300, yu40000, ha, hb, hc)
new_esEs9(LT, LT) → True
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs17(yu30, yu4000)
new_esEs25(yu300, yu40000, app(ty_Maybe, bdg)) → new_esEs8(yu300, yu40000, bdg)
new_esEs22(yu301, yu40001, ty_Char) → new_esEs15(yu301, yu40001)
new_esEs16(Left(yu300), Left(yu40000), ty_Float, ce) → new_esEs5(yu300, yu40000)
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_esEs16(Right(yu300), Right(yu40000), cd, app(app(app(ty_@3, fg), fh), ga)) → new_esEs11(yu300, yu40000, fg, fh, ga)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs4(yu30, yu4000, ty_Float) → new_esEs5(yu30, yu4000)
new_esEs16(Left(yu300), Left(yu40000), ty_@0, ce) → new_esEs7(yu300, yu40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), x1)
new_esEs8(Nothing, Nothing, x0)
new_esEs26(x0, x1, ty_Char)
new_esEs21(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_esEs8(Just(x0), Nothing, x1)
new_esEs9(GT, GT)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs16(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs4(x0, x1, ty_Bool)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs7(@0, @0)
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Nothing, Just(x0), x1)
new_esEs16(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(:(x0, x1), :(x2, x3), x4)
new_esEs8(Just(x0), Just(x1), ty_Char)
new_esEs4(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), ty_Bool)
new_esEs25(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Right(x0), Right(x1), x2, ty_Int)
new_esEs25(x0, x1, ty_@0)
new_esEs16(Right(x0), Right(x1), x2, ty_Float)
new_esEs16(Right(x0), Right(x1), x2, ty_Double)
new_esEs9(EQ, EQ)
new_esEs16(Right(x0), Right(x1), x2, ty_Integer)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_@0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs16(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs16(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Double)
new_esEs14(x0, x1)
new_esEs18([], [], x0)
new_esEs19(x0, x1, ty_Int)
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Left(x0), Right(x1), x2, x3)
new_esEs16(Right(x0), Left(x1), x2, x3)
new_esEs4(x0, x1, ty_Double)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs8(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs9(GT, LT)
new_esEs9(LT, GT)
new_esEs21(x0, x1, ty_Double)
new_esEs16(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs18([], :(x0, x1), x2)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Float)
new_esEs17(False, False)
new_esEs26(x0, x1, ty_Bool)
new_esEs9(EQ, GT)
new_esEs9(GT, EQ)
new_esEs16(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Float)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs8(Just(x0), Just(x1), ty_@0)
new_esEs16(Left(x0), Left(x1), ty_@0, x2)
new_esEs16(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primPlusNat1(Zero, Succ(x0))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Int)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs24(x0, x1, ty_Char)
new_esEs5(Float(x0, x1), Float(x2, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs8(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Float)
new_esEs6(Double(x0, x1), Double(x2, x3))
new_esEs21(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), app(ty_[], x2))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Zero)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Left(x0), Left(x1), ty_Char, x2)
new_primEqNat0(Zero, Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs16(Right(x0), Right(x1), x2, ty_Bool)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_esEs8(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs23(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_esEs8(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Float)
new_esEs8(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs23(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Bool)
new_esEs16(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, ty_Char)
new_esEs9(EQ, LT)
new_esEs9(LT, EQ)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primEqNat0(Succ(x0), Succ(x1))
new_asAs(False, x0)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), ty_Float, x2)
new_esEs8(Just(x0), Just(x1), ty_Ordering)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs17(True, False)
new_esEs17(False, True)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs18(:(x0, x1), [], x2)
new_esEs21(x0, x1, ty_Char)
new_primPlusNat1(Zero, Zero)
new_esEs26(x0, x1, ty_Int)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs16(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_@0)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Double)
new_esEs24(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs17(True, True)
new_esEs26(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Char)
new_esEs16(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs15(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Float)
new_esEs12(Integer(x0), Integer(x1))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_@0)
new_primEqNat0(Zero, Succ(x0))
new_asAs(True, x0)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(LT, LT)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs8(Just(x0), Just(x1), ty_Integer)
new_esEs16(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Left(x0), Left(x1), ty_Integer, x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
QDP
                      ↳ UsableRulesProof
                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup(Nothing, :(@2(Just(yu4000), yu401), yu41), ba, bb) → new_lookup(Nothing, yu41, ba, bb)

The TRS R consists of the following rules:

new_esEs21(yu300, yu40000, ty_Double) → new_esEs6(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Float) → new_esEs5(yu302, yu40002)
new_primPlusNat1(Succ(yu2900), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu2900, yu40001000)))
new_esEs25(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Double) → new_esEs6(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Char) → new_esEs15(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_esEs21(yu300, yu40000, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs6(yu30, yu4000)
new_esEs9(LT, GT) → False
new_esEs9(GT, LT) → False
new_esEs16(Left(yu300), Left(yu40000), app(ty_[], fc), ce) → new_esEs18(yu300, yu40000, fc)
new_esEs24(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs18(:(yu300, yu301), :(yu40000, yu40001), cf) → new_asAs(new_esEs24(yu300, yu40000, cf), new_esEs18(yu301, yu40001, cf))
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_esEs24(yu300, yu40000, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs23(yu302, yu40002, app(ty_Ratio, bbd)) → new_esEs10(yu302, yu40002, bbd)
new_esEs22(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs21(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs26(yu301, yu40001, app(ty_Ratio, bfb)) → new_esEs10(yu301, yu40001, bfb)
new_esEs26(yu301, yu40001, ty_Double) → new_esEs6(yu301, yu40001)
new_esEs21(yu300, yu40000, ty_Bool) → new_esEs17(yu300, yu40000)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs23(yu302, yu40002, app(app(app(ty_@3, bbe), bbf), bbg)) → new_esEs11(yu302, yu40002, bbe, bbf, bbg)
new_esEs4(yu30, yu4000, app(app(app(ty_@3, bg), bh), ca)) → new_esEs11(yu30, yu4000, bg, bh, ca)
new_esEs22(yu301, yu40001, ty_Bool) → new_esEs17(yu301, yu40001)
new_esEs9(GT, GT) → True
new_esEs24(yu300, yu40000, app(app(ty_@2, bdb), bdc)) → new_esEs13(yu300, yu40000, bdb, bdc)
new_esEs25(yu300, yu40000, ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), ty_Double) → new_esEs6(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Char) → new_esEs15(yu301, yu40001)
new_esEs26(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs24(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Char) → new_esEs15(yu302, yu40002)
new_esEs23(yu302, yu40002, app(ty_Maybe, bbc)) → new_esEs8(yu302, yu40002, bbc)
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs16(Left(yu300), Left(yu40000), app(ty_Maybe, eb), ce) → new_esEs8(yu300, yu40000, eb)
new_esEs17(True, True) → True
new_esEs8(Just(yu300), Just(yu40000), app(app(ty_@2, de), df)) → new_esEs13(yu300, yu40000, de, df)
new_esEs16(Right(yu300), Right(yu40000), cd, app(app(ty_Either, gd), ge)) → new_esEs16(yu300, yu40000, gd, ge)
new_esEs8(Just(yu300), Just(yu40000), app(app(app(ty_@3, db), dc), dd)) → new_esEs11(yu300, yu40000, db, dc, dd)
new_esEs23(yu302, yu40002, ty_Double) → new_esEs6(yu302, yu40002)
new_esEs25(yu300, yu40000, app(app(app(ty_@3, bea), beb), bec)) → new_esEs11(yu300, yu40000, bea, beb, bec)
new_esEs16(Right(yu300), Right(yu40000), cd, app(ty_[], gf)) → new_esEs18(yu300, yu40000, gf)
new_esEs4(yu30, yu4000, app(app(ty_@2, cb), cc)) → new_esEs13(yu30, yu4000, cb, cc)
new_esEs23(yu302, yu40002, ty_Integer) → new_esEs12(yu302, yu40002)
new_esEs16(Right(yu300), Right(yu40000), cd, app(ty_Maybe, fd)) → new_esEs8(yu300, yu40000, fd)
new_esEs12(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs22(yu301, yu40001, ty_Float) → new_esEs5(yu301, yu40001)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Ordering) → new_esEs9(yu302, yu40002)
new_esEs16(Left(yu300), Left(yu40000), app(app(app(ty_@3, ed), ee), ef), ce) → new_esEs11(yu300, yu40000, ed, ee, ef)
new_esEs26(yu301, yu40001, app(app(ty_@2, bff), bfg)) → new_esEs13(yu301, yu40001, bff, bfg)
new_esEs21(yu300, yu40000, app(ty_Ratio, gh)) → new_esEs10(yu300, yu40000, gh)
new_esEs8(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs9(yu300, yu40000)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs11(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), bg, bh, ca) → new_asAs(new_esEs21(yu300, yu40000, bg), new_asAs(new_esEs22(yu301, yu40001, bh), new_esEs23(yu302, yu40002, ca)))
new_esEs25(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs18([], :(yu40000, yu40001), cf) → False
new_esEs18(:(yu300, yu301), [], cf) → False
new_esEs23(yu302, yu40002, app(app(ty_@2, bbh), bca)) → new_esEs13(yu302, yu40002, bbh, bca)
new_esEs16(Left(yu300), Left(yu40000), app(app(ty_Either, fa), fb), ce) → new_esEs16(yu300, yu40000, fa, fb)
new_esEs16(Left(yu300), Left(yu40000), ty_Bool, ce) → new_esEs17(yu300, yu40000)
new_esEs22(yu301, yu40001, ty_Integer) → new_esEs12(yu301, yu40001)
new_esEs16(Left(yu300), Right(yu40000), cd, ce) → False
new_esEs16(Right(yu300), Left(yu40000), cd, ce) → False
new_esEs26(yu301, yu40001, app(app(app(ty_@3, bfc), bfd), bfe)) → new_esEs11(yu301, yu40001, bfc, bfd, bfe)
new_esEs23(yu302, yu40002, ty_Bool) → new_esEs17(yu302, yu40002)
new_esEs9(EQ, GT) → False
new_esEs9(GT, EQ) → False
new_esEs5(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs14(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs25(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), app(app(ty_Either, dg), dh)) → new_esEs16(yu300, yu40000, dg, dh)
new_esEs8(Nothing, Nothing, be) → True
new_esEs4(yu30, yu4000, app(ty_Maybe, be)) → new_esEs8(yu30, yu4000, be)
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs4(yu30, yu4000, app(ty_Ratio, bf)) → new_esEs10(yu30, yu4000, bf)
new_esEs21(yu300, yu40000, app(app(ty_@2, hd), he)) → new_esEs13(yu300, yu40000, hd, he)
new_esEs8(Just(yu300), Just(yu40000), ty_Int) → new_esEs14(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Double, ce) → new_esEs6(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Int) → new_esEs14(yu301, yu40001)
new_esEs19(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Ordering, ce) → new_esEs9(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Int) → new_esEs14(yu302, yu40002)
new_asAs(False, yu28) → False
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs8(Just(yu300), Just(yu40000), ty_@0) → new_esEs7(yu300, yu40000)
new_primEqNat0(Zero, Zero) → True
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs22(yu301, yu40001, app(ty_Maybe, baa)) → new_esEs8(yu301, yu40001, baa)
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_esEs18([], [], cf) → True
new_esEs25(yu300, yu40000, app(ty_[], beh)) → new_esEs18(yu300, yu40000, beh)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_[], bdf)) → new_esEs18(yu300, yu40000, bdf)
new_esEs22(yu301, yu40001, app(app(ty_Either, bah), bba)) → new_esEs16(yu301, yu40001, bah, bba)
new_esEs17(False, False) → True
new_esEs8(Just(yu300), Just(yu40000), ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, app(ty_[], cf)) → new_esEs18(yu30, yu4000, cf)
new_esEs17(False, True) → False
new_esEs17(True, False) → False
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs12(yu30, yu4000)
new_esEs21(yu300, yu40000, app(app(ty_Either, hf), hg)) → new_esEs16(yu300, yu40000, hf, hg)
new_esEs21(yu300, yu40000, app(ty_Maybe, gg)) → new_esEs8(yu300, yu40000, gg)
new_esEs15(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Integer, ce) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs26(yu301, yu40001, app(app(ty_Either, bfh), bga)) → new_esEs16(yu301, yu40001, bfh, bga)
new_esEs23(yu302, yu40002, ty_@0) → new_esEs7(yu302, yu40002)
new_esEs21(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), app(app(ty_@2, eg), eh), ce) → new_esEs13(yu300, yu40000, eg, eh)
new_esEs13(@2(yu300, yu301), @2(yu40000, yu40001), cb, cc) → new_asAs(new_esEs25(yu300, yu40000, cb), new_esEs26(yu301, yu40001, cc))
new_esEs16(Right(yu300), Right(yu40000), cd, app(app(ty_@2, gb), gc)) → new_esEs13(yu300, yu40000, gb, gc)
new_esEs8(Just(yu300), Just(yu40000), ty_Char) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Ratio, bcf)) → new_esEs10(yu300, yu40000, bcf)
new_esEs23(yu302, yu40002, app(app(ty_Either, bcb), bcc)) → new_esEs16(yu302, yu40002, bcb, bcc)
new_esEs22(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_primPlusNat0(Succ(yu290), yu4000100) → Succ(Succ(new_primPlusNat1(yu290, yu4000100)))
new_esEs20(yu301, yu40001, ty_Integer) → new_esEs12(yu301, yu40001)
new_esEs16(Left(yu300), Left(yu40000), ty_Int, ce) → new_esEs14(yu300, yu40000)
new_esEs22(yu301, yu40001, app(ty_[], bbb)) → new_esEs18(yu301, yu40001, bbb)
new_esEs22(yu301, yu40001, app(ty_Ratio, bab)) → new_esEs10(yu301, yu40001, bab)
new_esEs21(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), app(ty_Ratio, da)) → new_esEs10(yu300, yu40000, da)
new_esEs26(yu301, yu40001, ty_Integer) → new_esEs12(yu301, yu40001)
new_esEs8(Nothing, Just(yu40000), be) → False
new_esEs8(Just(yu300), Nothing, be) → False
new_esEs9(EQ, EQ) → True
new_esEs14(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu300, yu40000, ty_Double) → new_esEs6(yu300, yu40000)
new_esEs22(yu301, yu40001, app(app(ty_@2, baf), bag)) → new_esEs13(yu301, yu40001, baf, bag)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs26(yu301, yu40001, app(ty_Maybe, bfa)) → new_esEs8(yu301, yu40001, bfa)
new_primPlusNat1(Succ(yu2900), Zero) → Succ(yu2900)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs25(yu300, yu40000, ty_Char) → new_esEs15(yu300, yu40000)
new_esEs25(yu300, yu40000, app(ty_Ratio, bdh)) → new_esEs10(yu300, yu40000, bdh)
new_esEs21(yu300, yu40000, ty_Char) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Maybe, bce)) → new_esEs8(yu300, yu40000, bce)
new_esEs26(yu301, yu40001, ty_Bool) → new_esEs17(yu301, yu40001)
new_esEs9(LT, EQ) → False
new_esEs9(EQ, LT) → False
new_esEs20(yu301, yu40001, ty_Int) → new_esEs14(yu301, yu40001)
new_esEs21(yu300, yu40000, app(ty_[], hh)) → new_esEs18(yu300, yu40000, hh)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs4(yu30, yu4000, app(app(ty_Either, cd), ce)) → new_esEs16(yu30, yu4000, cd, ce)
new_esEs25(yu300, yu40000, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs15(yu30, yu4000)
new_esEs19(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_esEs25(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), app(ty_Ratio, ec), ce) → new_esEs10(yu300, yu40000, ec)
new_esEs22(yu301, yu40001, ty_Int) → new_esEs14(yu301, yu40001)
new_esEs24(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs26(yu301, yu40001, app(ty_[], bgb)) → new_esEs18(yu301, yu40001, bgb)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs26(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs25(yu300, yu40000, ty_Double) → new_esEs6(yu300, yu40000)
new_asAs(True, yu28) → yu28
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs22(yu301, yu40001, ty_Double) → new_esEs6(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_@0) → new_esEs7(yu30, yu4000)
new_esEs24(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), app(ty_Maybe, cg)) → new_esEs8(yu300, yu40000, cg)
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_esEs22(yu301, yu40001, app(app(app(ty_@3, bac), bad), bae)) → new_esEs11(yu301, yu40001, bac, bad, bae)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs14(yu30, yu4000)
new_esEs16(Right(yu300), Right(yu40000), cd, app(ty_Ratio, ff)) → new_esEs10(yu300, yu40000, ff)
new_esEs24(yu300, yu40000, app(app(app(ty_@3, bcg), bch), bda)) → new_esEs11(yu300, yu40000, bcg, bch, bda)
new_esEs26(yu301, yu40001, ty_Float) → new_esEs5(yu301, yu40001)
new_esEs8(Just(yu300), Just(yu40000), ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Char, ce) → new_esEs15(yu300, yu40000)
new_esEs21(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, app(app(ty_Either, bdd), bde)) → new_esEs16(yu300, yu40000, bdd, bde)
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs8(Just(yu300), Just(yu40000), app(ty_[], ea)) → new_esEs18(yu300, yu40000, ea)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Char) → new_esEs15(yu300, yu40000)
new_esEs6(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs14(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs25(yu300, yu40000, app(app(ty_@2, bed), bee)) → new_esEs13(yu300, yu40000, bed, bee)
new_esEs10(:%(yu300, yu301), :%(yu40000, yu40001), bf) → new_asAs(new_esEs19(yu300, yu40000, bf), new_esEs20(yu301, yu40001, bf))
new_esEs25(yu300, yu40000, app(app(ty_Either, bef), beg)) → new_esEs16(yu300, yu40000, bef, beg)
new_esEs7(@0, @0) → True
new_esEs23(yu302, yu40002, app(ty_[], bcd)) → new_esEs18(yu302, yu40002, bcd)
new_esEs21(yu300, yu40000, app(app(app(ty_@3, ha), hb), hc)) → new_esEs11(yu300, yu40000, ha, hb, hc)
new_esEs9(LT, LT) → True
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs17(yu30, yu4000)
new_esEs25(yu300, yu40000, app(ty_Maybe, bdg)) → new_esEs8(yu300, yu40000, bdg)
new_esEs22(yu301, yu40001, ty_Char) → new_esEs15(yu301, yu40001)
new_esEs16(Left(yu300), Left(yu40000), ty_Float, ce) → new_esEs5(yu300, yu40000)
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_esEs16(Right(yu300), Right(yu40000), cd, app(app(app(ty_@3, fg), fh), ga)) → new_esEs11(yu300, yu40000, fg, fh, ga)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs4(yu30, yu4000, ty_Float) → new_esEs5(yu30, yu4000)
new_esEs16(Left(yu300), Left(yu40000), ty_@0, ce) → new_esEs7(yu300, yu40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), x1)
new_esEs8(Nothing, Nothing, x0)
new_esEs26(x0, x1, ty_Char)
new_esEs21(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_esEs8(Just(x0), Nothing, x1)
new_esEs9(GT, GT)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs16(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs4(x0, x1, ty_Bool)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs7(@0, @0)
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Nothing, Just(x0), x1)
new_esEs16(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(:(x0, x1), :(x2, x3), x4)
new_esEs8(Just(x0), Just(x1), ty_Char)
new_esEs4(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), ty_Bool)
new_esEs25(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Right(x0), Right(x1), x2, ty_Int)
new_esEs25(x0, x1, ty_@0)
new_esEs16(Right(x0), Right(x1), x2, ty_Float)
new_esEs16(Right(x0), Right(x1), x2, ty_Double)
new_esEs9(EQ, EQ)
new_esEs16(Right(x0), Right(x1), x2, ty_Integer)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_@0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs16(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs16(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Double)
new_esEs14(x0, x1)
new_esEs18([], [], x0)
new_esEs19(x0, x1, ty_Int)
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Left(x0), Right(x1), x2, x3)
new_esEs16(Right(x0), Left(x1), x2, x3)
new_esEs4(x0, x1, ty_Double)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs8(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs9(GT, LT)
new_esEs9(LT, GT)
new_esEs21(x0, x1, ty_Double)
new_esEs16(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs18([], :(x0, x1), x2)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Float)
new_esEs17(False, False)
new_esEs26(x0, x1, ty_Bool)
new_esEs9(EQ, GT)
new_esEs9(GT, EQ)
new_esEs16(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Float)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs8(Just(x0), Just(x1), ty_@0)
new_esEs16(Left(x0), Left(x1), ty_@0, x2)
new_esEs16(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primPlusNat1(Zero, Succ(x0))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Int)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs24(x0, x1, ty_Char)
new_esEs5(Float(x0, x1), Float(x2, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs8(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Float)
new_esEs6(Double(x0, x1), Double(x2, x3))
new_esEs21(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), app(ty_[], x2))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Zero)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Left(x0), Left(x1), ty_Char, x2)
new_primEqNat0(Zero, Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs16(Right(x0), Right(x1), x2, ty_Bool)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_esEs8(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs23(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_esEs8(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Float)
new_esEs8(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs23(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Bool)
new_esEs16(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, ty_Char)
new_esEs9(EQ, LT)
new_esEs9(LT, EQ)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primEqNat0(Succ(x0), Succ(x1))
new_asAs(False, x0)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), ty_Float, x2)
new_esEs8(Just(x0), Just(x1), ty_Ordering)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs17(True, False)
new_esEs17(False, True)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs18(:(x0, x1), [], x2)
new_esEs21(x0, x1, ty_Char)
new_primPlusNat1(Zero, Zero)
new_esEs26(x0, x1, ty_Int)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs16(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_@0)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Double)
new_esEs24(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs17(True, True)
new_esEs26(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Char)
new_esEs16(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs15(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Float)
new_esEs12(Integer(x0), Integer(x1))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_@0)
new_primEqNat0(Zero, Succ(x0))
new_asAs(True, x0)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(LT, LT)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs8(Just(x0), Just(x1), ty_Integer)
new_esEs16(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Left(x0), Left(x1), ty_Integer, x2)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
                    ↳ QDP
                      ↳ UsableRulesProof
QDP
                          ↳ QReductionProof
                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup(Nothing, :(@2(Just(yu4000), yu401), yu41), ba, bb) → new_lookup(Nothing, yu41, ba, bb)

R is empty.
The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), x1)
new_esEs8(Nothing, Nothing, x0)
new_esEs26(x0, x1, ty_Char)
new_esEs21(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_esEs8(Just(x0), Nothing, x1)
new_esEs9(GT, GT)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs16(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs4(x0, x1, ty_Bool)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs7(@0, @0)
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Nothing, Just(x0), x1)
new_esEs16(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(:(x0, x1), :(x2, x3), x4)
new_esEs8(Just(x0), Just(x1), ty_Char)
new_esEs4(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), ty_Bool)
new_esEs25(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Right(x0), Right(x1), x2, ty_Int)
new_esEs25(x0, x1, ty_@0)
new_esEs16(Right(x0), Right(x1), x2, ty_Float)
new_esEs16(Right(x0), Right(x1), x2, ty_Double)
new_esEs9(EQ, EQ)
new_esEs16(Right(x0), Right(x1), x2, ty_Integer)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_@0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs16(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs16(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Double)
new_esEs14(x0, x1)
new_esEs18([], [], x0)
new_esEs19(x0, x1, ty_Int)
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Left(x0), Right(x1), x2, x3)
new_esEs16(Right(x0), Left(x1), x2, x3)
new_esEs4(x0, x1, ty_Double)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs8(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs9(GT, LT)
new_esEs9(LT, GT)
new_esEs21(x0, x1, ty_Double)
new_esEs16(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs18([], :(x0, x1), x2)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Float)
new_esEs17(False, False)
new_esEs26(x0, x1, ty_Bool)
new_esEs9(EQ, GT)
new_esEs9(GT, EQ)
new_esEs16(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Float)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs8(Just(x0), Just(x1), ty_@0)
new_esEs16(Left(x0), Left(x1), ty_@0, x2)
new_esEs16(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primPlusNat1(Zero, Succ(x0))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Int)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs24(x0, x1, ty_Char)
new_esEs5(Float(x0, x1), Float(x2, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs8(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Float)
new_esEs6(Double(x0, x1), Double(x2, x3))
new_esEs21(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), app(ty_[], x2))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Zero)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Left(x0), Left(x1), ty_Char, x2)
new_primEqNat0(Zero, Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs16(Right(x0), Right(x1), x2, ty_Bool)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_esEs8(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs23(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_esEs8(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Float)
new_esEs8(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs23(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Bool)
new_esEs16(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, ty_Char)
new_esEs9(EQ, LT)
new_esEs9(LT, EQ)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primEqNat0(Succ(x0), Succ(x1))
new_asAs(False, x0)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), ty_Float, x2)
new_esEs8(Just(x0), Just(x1), ty_Ordering)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs17(True, False)
new_esEs17(False, True)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs18(:(x0, x1), [], x2)
new_esEs21(x0, x1, ty_Char)
new_primPlusNat1(Zero, Zero)
new_esEs26(x0, x1, ty_Int)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs16(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_@0)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Double)
new_esEs24(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs17(True, True)
new_esEs26(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Char)
new_esEs16(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs15(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Float)
new_esEs12(Integer(x0), Integer(x1))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_@0)
new_primEqNat0(Zero, Succ(x0))
new_asAs(True, x0)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(LT, LT)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs8(Just(x0), Just(x1), ty_Integer)
new_esEs16(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Left(x0), Left(x1), ty_Integer, x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0(Succ(x0), x1)
new_esEs8(Nothing, Nothing, x0)
new_esEs26(x0, x1, ty_Char)
new_esEs21(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_esEs8(Just(x0), Nothing, x1)
new_esEs9(GT, GT)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs16(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs4(x0, x1, ty_Bool)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs7(@0, @0)
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Nothing, Just(x0), x1)
new_esEs16(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(:(x0, x1), :(x2, x3), x4)
new_esEs8(Just(x0), Just(x1), ty_Char)
new_esEs4(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), ty_Bool)
new_esEs25(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Right(x0), Right(x1), x2, ty_Int)
new_esEs25(x0, x1, ty_@0)
new_esEs16(Right(x0), Right(x1), x2, ty_Float)
new_esEs16(Right(x0), Right(x1), x2, ty_Double)
new_esEs9(EQ, EQ)
new_esEs16(Right(x0), Right(x1), x2, ty_Integer)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_@0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs16(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs16(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Double)
new_esEs14(x0, x1)
new_esEs18([], [], x0)
new_esEs19(x0, x1, ty_Int)
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Left(x0), Right(x1), x2, x3)
new_esEs16(Right(x0), Left(x1), x2, x3)
new_esEs4(x0, x1, ty_Double)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs8(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs9(GT, LT)
new_esEs9(LT, GT)
new_esEs21(x0, x1, ty_Double)
new_esEs16(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs18([], :(x0, x1), x2)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Float)
new_esEs17(False, False)
new_esEs26(x0, x1, ty_Bool)
new_esEs9(EQ, GT)
new_esEs9(GT, EQ)
new_esEs16(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Float)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs8(Just(x0), Just(x1), ty_@0)
new_esEs16(Left(x0), Left(x1), ty_@0, x2)
new_esEs16(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primPlusNat1(Zero, Succ(x0))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Int)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs24(x0, x1, ty_Char)
new_esEs5(Float(x0, x1), Float(x2, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs8(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Float)
new_esEs6(Double(x0, x1), Double(x2, x3))
new_esEs21(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), app(ty_[], x2))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Zero)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Left(x0), Left(x1), ty_Char, x2)
new_primEqNat0(Zero, Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs16(Right(x0), Right(x1), x2, ty_Bool)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_esEs8(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs23(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_esEs8(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Float)
new_esEs8(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs23(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Bool)
new_esEs16(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, ty_Char)
new_esEs9(EQ, LT)
new_esEs9(LT, EQ)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primEqNat0(Succ(x0), Succ(x1))
new_asAs(False, x0)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), ty_Float, x2)
new_esEs8(Just(x0), Just(x1), ty_Ordering)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs17(True, False)
new_esEs17(False, True)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs18(:(x0, x1), [], x2)
new_esEs21(x0, x1, ty_Char)
new_primPlusNat1(Zero, Zero)
new_esEs26(x0, x1, ty_Int)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs16(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_@0)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Double)
new_esEs24(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs17(True, True)
new_esEs26(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Char)
new_esEs16(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs15(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Float)
new_esEs12(Integer(x0), Integer(x1))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_@0)
new_primEqNat0(Zero, Succ(x0))
new_asAs(True, x0)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(LT, LT)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs8(Just(x0), Just(x1), ty_Integer)
new_esEs16(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Left(x0), Left(x1), ty_Integer, x2)



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
                    ↳ QDP
                      ↳ UsableRulesProof
                        ↳ QDP
                          ↳ QReductionProof
QDP
                              ↳ QDPSizeChangeProof
                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_lookup(Nothing, :(@2(Just(yu4000), yu401), yu41), ba, bb) → new_lookup(Nothing, yu41, ba, bb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ DependencyGraphProof
                  ↳ AND
                    ↳ QDP
QDP
                      ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup(Just(yu30), :(@2(Just(yu4000), yu401), yu41), ba, bb) → new_lookup1(yu30, yu4000, yu401, yu41, new_esEs4(yu30, yu4000, bb), ba, bb)
new_lookup1(yu11, yu12, yu13, yu14, False, bc, bd) → new_lookup(Just(yu11), yu14, bc, bd)
new_lookup(Just(yu30), :(@2(Nothing, yu401), yu41), ba, bb) → new_lookup(Just(yu30), yu41, ba, bb)

The TRS R consists of the following rules:

new_esEs21(yu300, yu40000, ty_Double) → new_esEs6(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Float) → new_esEs5(yu302, yu40002)
new_primPlusNat1(Succ(yu2900), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu2900, yu40001000)))
new_esEs25(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Double) → new_esEs6(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Char) → new_esEs15(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_esEs21(yu300, yu40000, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs6(yu30, yu4000)
new_esEs9(LT, GT) → False
new_esEs9(GT, LT) → False
new_esEs16(Left(yu300), Left(yu40000), app(ty_[], fc), ce) → new_esEs18(yu300, yu40000, fc)
new_esEs24(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs18(:(yu300, yu301), :(yu40000, yu40001), cf) → new_asAs(new_esEs24(yu300, yu40000, cf), new_esEs18(yu301, yu40001, cf))
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_esEs24(yu300, yu40000, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs23(yu302, yu40002, app(ty_Ratio, bbd)) → new_esEs10(yu302, yu40002, bbd)
new_esEs22(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs21(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs26(yu301, yu40001, app(ty_Ratio, bfb)) → new_esEs10(yu301, yu40001, bfb)
new_esEs26(yu301, yu40001, ty_Double) → new_esEs6(yu301, yu40001)
new_esEs21(yu300, yu40000, ty_Bool) → new_esEs17(yu300, yu40000)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs23(yu302, yu40002, app(app(app(ty_@3, bbe), bbf), bbg)) → new_esEs11(yu302, yu40002, bbe, bbf, bbg)
new_esEs4(yu30, yu4000, app(app(app(ty_@3, bg), bh), ca)) → new_esEs11(yu30, yu4000, bg, bh, ca)
new_esEs22(yu301, yu40001, ty_Bool) → new_esEs17(yu301, yu40001)
new_esEs9(GT, GT) → True
new_esEs24(yu300, yu40000, app(app(ty_@2, bdb), bdc)) → new_esEs13(yu300, yu40000, bdb, bdc)
new_esEs25(yu300, yu40000, ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), ty_Double) → new_esEs6(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Char) → new_esEs15(yu301, yu40001)
new_esEs26(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs24(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Char) → new_esEs15(yu302, yu40002)
new_esEs23(yu302, yu40002, app(ty_Maybe, bbc)) → new_esEs8(yu302, yu40002, bbc)
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs16(Left(yu300), Left(yu40000), app(ty_Maybe, eb), ce) → new_esEs8(yu300, yu40000, eb)
new_esEs17(True, True) → True
new_esEs8(Just(yu300), Just(yu40000), app(app(ty_@2, de), df)) → new_esEs13(yu300, yu40000, de, df)
new_esEs16(Right(yu300), Right(yu40000), cd, app(app(ty_Either, gd), ge)) → new_esEs16(yu300, yu40000, gd, ge)
new_esEs8(Just(yu300), Just(yu40000), app(app(app(ty_@3, db), dc), dd)) → new_esEs11(yu300, yu40000, db, dc, dd)
new_esEs23(yu302, yu40002, ty_Double) → new_esEs6(yu302, yu40002)
new_esEs25(yu300, yu40000, app(app(app(ty_@3, bea), beb), bec)) → new_esEs11(yu300, yu40000, bea, beb, bec)
new_esEs16(Right(yu300), Right(yu40000), cd, app(ty_[], gf)) → new_esEs18(yu300, yu40000, gf)
new_esEs4(yu30, yu4000, app(app(ty_@2, cb), cc)) → new_esEs13(yu30, yu4000, cb, cc)
new_esEs23(yu302, yu40002, ty_Integer) → new_esEs12(yu302, yu40002)
new_esEs16(Right(yu300), Right(yu40000), cd, app(ty_Maybe, fd)) → new_esEs8(yu300, yu40000, fd)
new_esEs12(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs22(yu301, yu40001, ty_Float) → new_esEs5(yu301, yu40001)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Ordering) → new_esEs9(yu302, yu40002)
new_esEs16(Left(yu300), Left(yu40000), app(app(app(ty_@3, ed), ee), ef), ce) → new_esEs11(yu300, yu40000, ed, ee, ef)
new_esEs26(yu301, yu40001, app(app(ty_@2, bff), bfg)) → new_esEs13(yu301, yu40001, bff, bfg)
new_esEs21(yu300, yu40000, app(ty_Ratio, gh)) → new_esEs10(yu300, yu40000, gh)
new_esEs8(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs9(yu300, yu40000)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs11(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), bg, bh, ca) → new_asAs(new_esEs21(yu300, yu40000, bg), new_asAs(new_esEs22(yu301, yu40001, bh), new_esEs23(yu302, yu40002, ca)))
new_esEs25(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs18([], :(yu40000, yu40001), cf) → False
new_esEs18(:(yu300, yu301), [], cf) → False
new_esEs23(yu302, yu40002, app(app(ty_@2, bbh), bca)) → new_esEs13(yu302, yu40002, bbh, bca)
new_esEs16(Left(yu300), Left(yu40000), app(app(ty_Either, fa), fb), ce) → new_esEs16(yu300, yu40000, fa, fb)
new_esEs16(Left(yu300), Left(yu40000), ty_Bool, ce) → new_esEs17(yu300, yu40000)
new_esEs22(yu301, yu40001, ty_Integer) → new_esEs12(yu301, yu40001)
new_esEs16(Left(yu300), Right(yu40000), cd, ce) → False
new_esEs16(Right(yu300), Left(yu40000), cd, ce) → False
new_esEs26(yu301, yu40001, app(app(app(ty_@3, bfc), bfd), bfe)) → new_esEs11(yu301, yu40001, bfc, bfd, bfe)
new_esEs23(yu302, yu40002, ty_Bool) → new_esEs17(yu302, yu40002)
new_esEs9(EQ, GT) → False
new_esEs9(GT, EQ) → False
new_esEs5(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs14(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs25(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), app(app(ty_Either, dg), dh)) → new_esEs16(yu300, yu40000, dg, dh)
new_esEs8(Nothing, Nothing, be) → True
new_esEs4(yu30, yu4000, app(ty_Maybe, be)) → new_esEs8(yu30, yu4000, be)
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs4(yu30, yu4000, app(ty_Ratio, bf)) → new_esEs10(yu30, yu4000, bf)
new_esEs21(yu300, yu40000, app(app(ty_@2, hd), he)) → new_esEs13(yu300, yu40000, hd, he)
new_esEs8(Just(yu300), Just(yu40000), ty_Int) → new_esEs14(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Double, ce) → new_esEs6(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Int) → new_esEs14(yu301, yu40001)
new_esEs19(yu300, yu40000, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Ordering, ce) → new_esEs9(yu300, yu40000)
new_esEs23(yu302, yu40002, ty_Int) → new_esEs14(yu302, yu40002)
new_asAs(False, yu28) → False
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs8(Just(yu300), Just(yu40000), ty_@0) → new_esEs7(yu300, yu40000)
new_primEqNat0(Zero, Zero) → True
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Int) → new_esEs14(yu300, yu40000)
new_esEs22(yu301, yu40001, app(ty_Maybe, baa)) → new_esEs8(yu301, yu40001, baa)
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_esEs18([], [], cf) → True
new_esEs25(yu300, yu40000, app(ty_[], beh)) → new_esEs18(yu300, yu40000, beh)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_[], bdf)) → new_esEs18(yu300, yu40000, bdf)
new_esEs22(yu301, yu40001, app(app(ty_Either, bah), bba)) → new_esEs16(yu301, yu40001, bah, bba)
new_esEs17(False, False) → True
new_esEs8(Just(yu300), Just(yu40000), ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, app(ty_[], cf)) → new_esEs18(yu30, yu4000, cf)
new_esEs17(False, True) → False
new_esEs17(True, False) → False
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs12(yu30, yu4000)
new_esEs21(yu300, yu40000, app(app(ty_Either, hf), hg)) → new_esEs16(yu300, yu40000, hf, hg)
new_esEs21(yu300, yu40000, app(ty_Maybe, gg)) → new_esEs8(yu300, yu40000, gg)
new_esEs15(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Integer, ce) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, ty_Bool) → new_esEs17(yu300, yu40000)
new_esEs26(yu301, yu40001, app(app(ty_Either, bfh), bga)) → new_esEs16(yu301, yu40001, bfh, bga)
new_esEs23(yu302, yu40002, ty_@0) → new_esEs7(yu302, yu40002)
new_esEs21(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), app(app(ty_@2, eg), eh), ce) → new_esEs13(yu300, yu40000, eg, eh)
new_esEs13(@2(yu300, yu301), @2(yu40000, yu40001), cb, cc) → new_asAs(new_esEs25(yu300, yu40000, cb), new_esEs26(yu301, yu40001, cc))
new_esEs16(Right(yu300), Right(yu40000), cd, app(app(ty_@2, gb), gc)) → new_esEs13(yu300, yu40000, gb, gc)
new_esEs8(Just(yu300), Just(yu40000), ty_Char) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Ratio, bcf)) → new_esEs10(yu300, yu40000, bcf)
new_esEs23(yu302, yu40002, app(app(ty_Either, bcb), bcc)) → new_esEs16(yu302, yu40002, bcb, bcc)
new_esEs22(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_primPlusNat0(Succ(yu290), yu4000100) → Succ(Succ(new_primPlusNat1(yu290, yu4000100)))
new_esEs20(yu301, yu40001, ty_Integer) → new_esEs12(yu301, yu40001)
new_esEs16(Left(yu300), Left(yu40000), ty_Int, ce) → new_esEs14(yu300, yu40000)
new_esEs22(yu301, yu40001, app(ty_[], bbb)) → new_esEs18(yu301, yu40001, bbb)
new_esEs22(yu301, yu40001, app(ty_Ratio, bab)) → new_esEs10(yu301, yu40001, bab)
new_esEs21(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), app(ty_Ratio, da)) → new_esEs10(yu300, yu40000, da)
new_esEs26(yu301, yu40001, ty_Integer) → new_esEs12(yu301, yu40001)
new_esEs8(Nothing, Just(yu40000), be) → False
new_esEs8(Just(yu300), Nothing, be) → False
new_esEs9(EQ, EQ) → True
new_esEs14(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu300, yu40000, ty_Double) → new_esEs6(yu300, yu40000)
new_esEs22(yu301, yu40001, app(app(ty_@2, baf), bag)) → new_esEs13(yu301, yu40001, baf, bag)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs26(yu301, yu40001, app(ty_Maybe, bfa)) → new_esEs8(yu301, yu40001, bfa)
new_primPlusNat1(Succ(yu2900), Zero) → Succ(yu2900)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs25(yu300, yu40000, ty_Char) → new_esEs15(yu300, yu40000)
new_esEs25(yu300, yu40000, app(ty_Ratio, bdh)) → new_esEs10(yu300, yu40000, bdh)
new_esEs21(yu300, yu40000, ty_Char) → new_esEs15(yu300, yu40000)
new_esEs24(yu300, yu40000, app(ty_Maybe, bce)) → new_esEs8(yu300, yu40000, bce)
new_esEs26(yu301, yu40001, ty_Bool) → new_esEs17(yu301, yu40001)
new_esEs9(LT, EQ) → False
new_esEs9(EQ, LT) → False
new_esEs20(yu301, yu40001, ty_Int) → new_esEs14(yu301, yu40001)
new_esEs21(yu300, yu40000, app(ty_[], hh)) → new_esEs18(yu300, yu40000, hh)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs4(yu30, yu4000, app(app(ty_Either, cd), ce)) → new_esEs16(yu30, yu4000, cd, ce)
new_esEs25(yu300, yu40000, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs15(yu30, yu4000)
new_esEs19(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_esEs25(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), app(ty_Ratio, ec), ce) → new_esEs10(yu300, yu40000, ec)
new_esEs22(yu301, yu40001, ty_Int) → new_esEs14(yu301, yu40001)
new_esEs24(yu300, yu40000, ty_Ordering) → new_esEs9(yu300, yu40000)
new_esEs26(yu301, yu40001, app(ty_[], bgb)) → new_esEs18(yu301, yu40001, bgb)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs26(yu301, yu40001, ty_Ordering) → new_esEs9(yu301, yu40001)
new_esEs25(yu300, yu40000, ty_Double) → new_esEs6(yu300, yu40000)
new_asAs(True, yu28) → yu28
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs22(yu301, yu40001, ty_Double) → new_esEs6(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_@0) → new_esEs7(yu30, yu4000)
new_esEs24(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs8(Just(yu300), Just(yu40000), app(ty_Maybe, cg)) → new_esEs8(yu300, yu40000, cg)
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Float) → new_esEs5(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs9(yu30, yu4000)
new_esEs22(yu301, yu40001, app(app(app(ty_@3, bac), bad), bae)) → new_esEs11(yu301, yu40001, bac, bad, bae)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs14(yu30, yu4000)
new_esEs16(Right(yu300), Right(yu40000), cd, app(ty_Ratio, ff)) → new_esEs10(yu300, yu40000, ff)
new_esEs24(yu300, yu40000, app(app(app(ty_@3, bcg), bch), bda)) → new_esEs11(yu300, yu40000, bcg, bch, bda)
new_esEs26(yu301, yu40001, ty_Float) → new_esEs5(yu301, yu40001)
new_esEs8(Just(yu300), Just(yu40000), ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs16(Left(yu300), Left(yu40000), ty_Char, ce) → new_esEs15(yu300, yu40000)
new_esEs21(yu300, yu40000, ty_Integer) → new_esEs12(yu300, yu40000)
new_esEs24(yu300, yu40000, app(app(ty_Either, bdd), bde)) → new_esEs16(yu300, yu40000, bdd, bde)
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs8(Just(yu300), Just(yu40000), app(ty_[], ea)) → new_esEs18(yu300, yu40000, ea)
new_esEs16(Right(yu300), Right(yu40000), cd, ty_Char) → new_esEs15(yu300, yu40000)
new_esEs6(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs14(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs25(yu300, yu40000, app(app(ty_@2, bed), bee)) → new_esEs13(yu300, yu40000, bed, bee)
new_esEs10(:%(yu300, yu301), :%(yu40000, yu40001), bf) → new_asAs(new_esEs19(yu300, yu40000, bf), new_esEs20(yu301, yu40001, bf))
new_esEs25(yu300, yu40000, app(app(ty_Either, bef), beg)) → new_esEs16(yu300, yu40000, bef, beg)
new_esEs7(@0, @0) → True
new_esEs23(yu302, yu40002, app(ty_[], bcd)) → new_esEs18(yu302, yu40002, bcd)
new_esEs21(yu300, yu40000, app(app(app(ty_@3, ha), hb), hc)) → new_esEs11(yu300, yu40000, ha, hb, hc)
new_esEs9(LT, LT) → True
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs17(yu30, yu4000)
new_esEs25(yu300, yu40000, app(ty_Maybe, bdg)) → new_esEs8(yu300, yu40000, bdg)
new_esEs22(yu301, yu40001, ty_Char) → new_esEs15(yu301, yu40001)
new_esEs16(Left(yu300), Left(yu40000), ty_Float, ce) → new_esEs5(yu300, yu40000)
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_esEs16(Right(yu300), Right(yu40000), cd, app(app(app(ty_@3, fg), fh), ga)) → new_esEs11(yu300, yu40000, fg, fh, ga)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs4(yu30, yu4000, ty_Float) → new_esEs5(yu30, yu4000)
new_esEs16(Left(yu300), Left(yu40000), ty_@0, ce) → new_esEs7(yu300, yu40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), x1)
new_esEs8(Nothing, Nothing, x0)
new_esEs26(x0, x1, ty_Char)
new_esEs21(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_esEs8(Just(x0), Nothing, x1)
new_esEs9(GT, GT)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs16(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs4(x0, x1, ty_Bool)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs7(@0, @0)
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Nothing, Just(x0), x1)
new_esEs16(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(:(x0, x1), :(x2, x3), x4)
new_esEs8(Just(x0), Just(x1), ty_Char)
new_esEs4(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), ty_Bool)
new_esEs25(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Right(x0), Right(x1), x2, ty_Int)
new_esEs25(x0, x1, ty_@0)
new_esEs16(Right(x0), Right(x1), x2, ty_Float)
new_esEs16(Right(x0), Right(x1), x2, ty_Double)
new_esEs9(EQ, EQ)
new_esEs16(Right(x0), Right(x1), x2, ty_Integer)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_@0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs16(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs16(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Double)
new_esEs14(x0, x1)
new_esEs18([], [], x0)
new_esEs19(x0, x1, ty_Int)
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Neg(x1))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Left(x0), Right(x1), x2, x3)
new_esEs16(Right(x0), Left(x1), x2, x3)
new_esEs4(x0, x1, ty_Double)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs8(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs9(GT, LT)
new_esEs9(LT, GT)
new_esEs21(x0, x1, ty_Double)
new_esEs16(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs18([], :(x0, x1), x2)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Float)
new_esEs17(False, False)
new_esEs26(x0, x1, ty_Bool)
new_esEs9(EQ, GT)
new_esEs9(GT, EQ)
new_esEs16(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Float)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs8(Just(x0), Just(x1), ty_@0)
new_esEs16(Left(x0), Left(x1), ty_@0, x2)
new_esEs16(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primPlusNat1(Zero, Succ(x0))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Int)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs24(x0, x1, ty_Char)
new_esEs5(Float(x0, x1), Float(x2, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs8(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Float)
new_esEs6(Double(x0, x1), Double(x2, x3))
new_esEs21(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), app(ty_[], x2))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Zero)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Left(x0), Left(x1), ty_Char, x2)
new_primEqNat0(Zero, Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs16(Right(x0), Right(x1), x2, ty_Bool)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_esEs8(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs23(x0, x1, ty_Double)
new_primMulNat0(Zero, Zero)
new_esEs8(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Float)
new_esEs8(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs23(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Double)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Bool)
new_esEs16(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, ty_Char)
new_esEs9(EQ, LT)
new_esEs9(LT, EQ)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primEqNat0(Succ(x0), Succ(x1))
new_asAs(False, x0)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), ty_Float, x2)
new_esEs8(Just(x0), Just(x1), ty_Ordering)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs17(True, False)
new_esEs17(False, True)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs18(:(x0, x1), [], x2)
new_esEs21(x0, x1, ty_Char)
new_primPlusNat1(Zero, Zero)
new_esEs26(x0, x1, ty_Int)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs16(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_@0)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Double)
new_esEs24(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs17(True, True)
new_esEs26(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Char)
new_esEs16(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs15(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Float)
new_esEs12(Integer(x0), Integer(x1))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_@0)
new_primEqNat0(Zero, Succ(x0))
new_asAs(True, x0)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(LT, LT)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs8(Just(x0), Just(x1), ty_Integer)
new_esEs16(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Left(x0), Left(x1), ty_Integer, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: